const std = @import("std");
const TerVec = @import("tervec.zig");

pub const ParseError = error{
    FileNotFound,
    InvalidFormat,
    NoHeader,
    EmptyClause,
    OutOfMemory,
};

pub const CnfResult = struct {
    vecs: std.ArrayList(TerVec),
    vars: usize,
};

/// Parses a DIMACS CNF file into a list of TerVec instances
/// Caller owns the returned ArrayList and must call deinit()
pub fn parseCNF(allocator: std.mem.Allocator, path: []const u8) !CnfResult {
    // Open the file
    const file = try std.fs.cwd().openFile(path, .{});
    defer file.close();

    var buf_reader = std.io.bufferedReader(file.reader());
    var in_stream = buf_reader.reader();

    // Create list to store TerVecs
    var vecs = std.ArrayList(TerVec).init(allocator);
    errdefer vecs.deinit();

    var vars: ?usize = null;
    var buf: [1024]u8 = undefined;

    // Read file line by line
    while (try in_stream.readUntilDelimiterOrEof(&buf, '\n')) |line| {
        // Skip empty lines and comments
        if (line.len == 0 or line[0] == 'c' or line[0] == '%') continue;

        // Parse header
        if (std.mem.startsWith(u8, std.mem.trim(u8, line, " \t\r\n"), "p cnf")) {
            var iter = std.mem.tokenizeScalar(u8, line, ' ');
            _ = iter.next(); // skip "p"
            _ = iter.next(); // skip "cnf"

            const num_vars_str = iter.next() orelse return ParseError.InvalidFormat;
            vars = try std.fmt.parseInt(usize, num_vars_str, 10);

            // We don't need the clause count, but parse it to validate format
            _ = iter.next() orelse return ParseError.InvalidFormat;
            continue;
        }

        // Ensure we've seen the header
        if (vars == null) return ParseError.NoHeader;

        // Parse clause
        var terms = std.ArrayList(i32).init(allocator);
        defer terms.deinit();

        var iter = std.mem.tokenizeScalar(u8, line, ' ');
        var has_literals = false;

        while (iter.next()) |term_str| {
            if (term_str.len == 0) continue;
            const term = try std.fmt.parseInt(i16, term_str, 10);

            if (term == 0) {
                if (!has_literals) return ParseError.EmptyClause;

                // Truncate each term to the width of SegAdr + BitAdr
                const width = TerVec.BitAdr + TerVec.SegAdr;
                const mask = (1 << width) - 1;
                var truncated_terms = try allocator.alloc(TerVec.i(width), terms.items.len);
                defer allocator.free(truncated_terms);
                for (terms.items, 0..) |t, i| {
                    // Zig's signed mask: preserve sign, mask abs value
                    truncated_terms[i] = @as(TerVec.i(width), if (t < 0) -(@as(i(width), -t) & mask) else (t & mask));
                }

                // Create TerVec and add literals
                var vec = TerVec.zero();
                try vec.set(truncated_terms);
                try vecs.append(vec);
                break;
            } else {
                has_literals = true;
                try terms.append(term);
            }
        }
    }

    return CnfResult{
        .vecs = vecs,
        .vars = vars orelse return ParseError.NoHeader,
    };
}

/// Print statistics about the parsed CNF formula
pub fn printStats(result: CnfResult) void {
    std.debug.print("CNF Statistics:\n", .{});
    std.debug.print("  Variables: {d}\n", .{result.vars});
    std.debug.print("  Clauses: {d}\n", .{result.vecs.items.len});
}

test "parseCNF - basic test" {
    // TODO: Add test cases once you have a sample CNF file
    // For now, this is a placeholder to remind you to add tests
}
